在像 Haskell 或 Idris 這樣的語言中，是否可以創建一種資料型別來檢查函式的輸入向量是否是單一的？也就是說，我可以創建一個資料型別 SumsToOne 來檢查向量加起來是否為 1 等？
uj5u.com熱心網友回復：
是的。在伊德里斯，就像你說的那樣。您可以用元素總和為一的證明包裝一個串列
data SumsToOne : Type where
STO : (xs : List Int) -> {auto prf : sum xs = 1} -> SumsToOne
盡管如果按資料型別指的是證明，而不是元素，您可以
go : (xs : List Int) -> {auto prf : sum xs = 1} -> <whatever you're returning>
證明是型別的sums xs = 1。prf只是函式引數名稱， auto這意味著如果可以的話，Idris 會為您找到證明。
我不知道這是否適用于浮點元素。
轉載請註明出處，本文鏈接：https://www.uj5u.com/qianduan/462862.html
一個個人用的瀏覽器首頁，可以把一下常用的網站放在這里，平常打開會比較方便。 第一步，HTML代碼 <script src=https://www.cnblogs.com/szharf/p/"js/jquery-3.4.1.min.js"></script> <div id="navigate"> <ul> <li class="labels labels_1"> ......
uj5u.com 2020-09-10 04:38:47 more最近因為寫一個js函式，需要用到$(window).height(); 由于手寫demo的時候，過于自信，其實對前端方面的認識也不夠體系，用文本檔案直接敲出來的html代碼，第一行沒有加上<!DOCTYPE html> 導致了$(window).height();的結果直接是整個document的高 ......
uj5u.com 2020-09-10 04:38:52 moreWordPress博客網站程式在進行升級前，必須要做好網站資料的備份，這個問題良家佐言是遇見過的；在剛開始接觸WordPress博客程式的時候，因為升級問題和博客網站的修改的一些嘗試，良家佐言是吃盡了苦頭。因為購買的是西部數碼的空間和域名，每當佐言把自己的WordPress博客網站搞到一塌糊涂的時候 ......
uj5u.com 2020-09-10 04:39:30 moreWordPress是一款個人博客系統，受到英文博客愛好者和中文博客愛好者的追捧，并逐步演化成一款內容管理系統軟體；它是使用PHP語言和MySQL資料庫開發的,用戶可以在支持PHP和MySQL資料庫的服務器上使用自己的博客。每一次WordPress程式的更新，就會牽動無數WordPress愛好者的心， ......
uj5u.com 2020-09-10 04:39:49 more網頁中常見的一種效果，首字改變樣式或者首行改變樣式，效果如下圖。 代碼： <!DOCTYPE html> <html lang="en"> <head> <meta charset="UTF-8"> <meta name="viewport" content="width=device-width, ......
uj5u.com 2020-09-10 04:40:09 more1 <style>2 body{background-image:url(https://uploadbeta.com/api/pictures/random/?key=BingEverydayWallpaperPicture); 3 background-size:cover;background ......
uj5u.com 2020-09-10 04:40:16 moreHTML詳解 初識HTML Hyper Text Markup Language（超文本標記語言） 1 <!--DOCTYPE:告訴瀏覽器我們要使用什么規范--> 2 <!DOCTYPE html> 3 <html lang="en"> 4 <head> 5 <!--meta 描述性的標簽，描述一些 ......
uj5u.com 2020-09-10 04:40:33 more好家伙,我的包終于開發完啦 歡迎使用胖虎的飛機大戰包!! 為你的主頁添加色彩 這是一個有趣的網頁小游戲包,使用canvas和js開發 使用ES6模塊化開發 效果圖如下: (覺得圖片太sb的可以自己改) 代碼已開源!! Git: https://gitee.com/tang-and-han-dynas ......
uj5u.com 2023-04-20 07:59:23 more入職多年，面對生產環境，盡管都是小心翼翼，慎之又慎，還是難免捅出簍子。輕則滿頭大汗，面紅耳赤。重則系統停擺，損失資金。每一個生產事故的背后，都是寶貴的經驗和教訓，都是專案成員的血淚史。為了更好地防范和遏制今后的各類事故，特開此專題，長期更新和記錄大大小小的各類事故。有些是親身經歷，有些是經人耳傳口授 ......
uj5u.com 2023-04-18 07:55:04 more這里給大家分享我在網上總結出來的一些知識，希望對大家有所幫助 打開游戲界面，看到一個畫面簡潔、卻又富有挑戰性的游戲。螢屏上，有一個白色的矩形框，里面不斷下落著各種單詞，而我需要迅速地輸入這些單詞。如果我輸入的單詞與螢屏上的單詞匹配，那么我就可以獲得得分；如果我輸入的單詞錯誤或者時間過長，那么我就會輸 ......
uj5u.com 2023-04-04 08:35:30 more在學習網路之前，了解它的歷史能夠幫助我們明白為何它會發展為如今這個樣子，引發探究網路的興趣。下面的這張圖片就展示了“互聯網”誕生至今的發展歷程。 ......
uj5u.com 2023-03-16 11:00:15 more//11.開啟藍牙配接器 openBluetoothAdapter //21.開始搜索藍牙設備 startBluetoothDevicesDiscovery //31.開啟監聽搜索藍牙設備 onBluetoothDeviceFound //30.停止監聽搜索藍牙設備 offBluetoothDevi ......
uj5u.com 2023-03-15 09:06:45 more<!DOCTYPE html> <html> <head> <meta charset="utf-8"> <title>canves</title> <style> #canvas { cursor:url(../images/pen.png),crosshair; } #canvasdiv{ bo ......
uj5u.com 2023-02-15 08:56:31 more手機端 H5 實作自定義拍照界面也可以使用 MediaDevices API 和 <video> 標簽來實作，和在桌面端做法基本一致。 首先，使用 MediaDevices.getUserMedia() 方法獲取攝像頭媒體流，并將其傳遞給 <video> 標簽進行渲染。 接著，使用 HTML 的 < ......
uj5u.com 2023-01-12 07:58:22 more這里給大家分享我在網上總結出來的一些知識，希望對大家有所幫助 短視頻已經無數不在了，但是主體還是使用 app 來承載的。本文講述 H5 如何實作 app 的視頻滑動體驗。 無聲勝有聲，一圖頂百辯，且看下圖： 網址鏈接（需在微信或者手Q中瀏覽） 從上圖可以看到，我們主要實作的功能也是本文要講解的有： ......
uj5u.com 2023-01-04 07:29:05 more從 1989 年萬維網（www）誕生，HTTP（HyperText Transfer Protocol）經歷了眾多版本迭代，WebSocket 也在期間萌芽。1991 年 HTTP0.9 被發明。1996 年出現了 HTTP1.0。2015 年 HTTP2 正式發布。2020 年 HTTP3 或能正... ......
uj5u.com 2022-12-24 06:56:02 more??一、form表單是什么
??二、form表單的屬性
??三、input中的各種Type屬性值
??四、標簽 ......